//
// THIS FILE IS AUTOMATICALLY GENERATED!!
//
// Generated at Thu 06-Dec-2012 by the VDM++ to JAVA Code Generator
// (v8.0 - Mon 09-Jul-2007 09:32:40)
//
// Supported compilers:
// jdk1.4
//

// ***** VDMTOOLS START Name=HeaderComment KEEP=NO
// ***** VDMTOOLS END Name=HeaderComment

// ***** VDMTOOLS START Name=package KEEP=NO
// ***** VDMTOOLS END Name=package

// ***** VDMTOOLS START Name=imports KEEP=NO

import jp.co.csk.vdm.toolbox.VDM.*;
import java.util.*;
import jp.co.csk.vdm.toolbox.VDM.jdk.*;
// ***** VDMTOOLS END Name=imports



public class UML implements EvaluatePP {

// ***** VDMTOOLS START Name=vdmComp KEEP=NO
  static UTIL.VDMCompare vdmComp = new UTIL.VDMCompare();
// ***** VDMTOOLS END Name=vdmComp

// ***** VDMTOOLS START Name=startState KEEP=NO
  protected volatile State startState = null;
// ***** VDMTOOLS END Name=startState

// ***** VDMTOOLS START Name=allStates KEEP=NO
  public volatile HashMap allStates = new HashMap();
// ***** VDMTOOLS END Name=allStates

// ***** VDMTOOLS START Name=sentinel KEEP=NO
  volatile Sentinel sentinel;
// ***** VDMTOOLS END Name=sentinel


// ***** VDMTOOLS START Name=UMLSentinel KEEP=NO
  class UMLSentinel extends Sentinel {

    public final int UML = 0;

    public final int states = 1;

    public final int isEmpty = 2;

    public final int addState = 3;

    public final int getState = 4;

    public final int mapStates = 5;

    public final int verifyPath = 6;

    public final int searchStart = 7;

    public final int addStartState = 8;

    public final int getStartState = 9;

    public final int stateExists_u_u1_un_uState = 10;

    public final int stateExists_u_u1_un_uString = 11;

    public final int nr_functions = 12;


    public UMLSentinel () throws CGException {}


    public UMLSentinel (EvaluatePP instance) throws CGException {
      init(nr_functions, instance);
    }

  }
// ***** VDMTOOLS END Name=UMLSentinel
;

// ***** VDMTOOLS START Name=evaluatePP KEEP=NO
  public Boolean evaluatePP (int fnr) throws CGException {
    return new Boolean(true);
  }
// ***** VDMTOOLS END Name=evaluatePP


// ***** VDMTOOLS START Name=setSentinel KEEP=NO
  public void setSentinel () {
    try {
      sentinel = new UMLSentinel(this);
    }
    catch (CGException e) {
      System.out.println(e.getMessage());
    }
  }
// ***** VDMTOOLS END Name=setSentinel


// ***** VDMTOOLS START Name=UML KEEP=NO
  public UML () throws CGException {
    try {

      setSentinel();
      allStates = new HashMap();
    }
    catch (Exception e){

      e.printStackTrace(System.out);
      System.out.println(e.getMessage());
    }
  }
// ***** VDMTOOLS END Name=UML


// ***** VDMTOOLS START Name=UML KEEP=NO
  public UML (final State sState, final HashSet states) throws CGException {

    try {

      setSentinel();
      allStates = new HashMap();
    }
    catch (Exception e){

      e.printStackTrace(System.out);
      System.out.println(e.getMessage());
    }
    if (!this.pre_UML(sState, states).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in UML");
    {

      mapStates(states);
      addStartState((State) sState);
    }
  }
// ***** VDMTOOLS END Name=UML


// ***** VDMTOOLS START Name=pre_UML KEEP=NO
  public Boolean pre_UML (final State sState, final HashSet states) throws CGException {
    return new Boolean((new Integer(states.size()).intValue()) > (new Integer(0).intValue()));
  }
// ***** VDMTOOLS END Name=pre_UML


// ***** VDMTOOLS START Name=mapStates KEEP=NO
  private void mapStates (final HashSet states_1) throws CGException {

    if (!this.pre_mapStates(states_1).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in mapStates");
    sentinel.entering(((UMLSentinel) sentinel).mapStates);
    try {
      return;
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).mapStates);
    }
  }
// ***** VDMTOOLS END Name=mapStates


// ***** VDMTOOLS START Name=pre_mapStates KEEP=NO
  private Boolean pre_mapStates (final HashSet states_1) throws CGException {

    Boolean varRes_2 = null;
    boolean tmpQuant_3 = true;
    {

      State s = null;
      {
        for (Iterator enm_9 = states_1.iterator(); enm_9.hasNext() && tmpQuant_3; ) {

          State elem_8 = (State) enm_9.next();
          s = (State) elem_8;
          if (addState((State) s).booleanValue()) {}
          else 
            tmpQuant_3 = false;
        }
      }
    }
    varRes_2 = new Boolean(tmpQuant_3);
    return varRes_2;
  }
// ***** VDMTOOLS END Name=pre_mapStates


// ***** VDMTOOLS START Name=addState KEEP=NO
  public Boolean addState (final State state) throws CGException {

    sentinel.entering(((UMLSentinel) sentinel).addState);
    try {

      String md_3 = null;
      md_3 = state.getName();
      allStates.put(md_3, state);
      return new Boolean(true);
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).addState);
    }
  }
// ***** VDMTOOLS END Name=addState


// ***** VDMTOOLS START Name=states KEEP=NO
  public HashMap states () throws CGException {

    sentinel.entering(((UMLSentinel) sentinel).states);
    try {
      return allStates;
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).states);
    }
  }
// ***** VDMTOOLS END Name=states


// ***** VDMTOOLS START Name=addStartState KEEP=NO
  public void addStartState (final State x) throws CGException {

    if (!this.pre_addStartState(x).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in addStartState");
    sentinel.entering(((UMLSentinel) sentinel).addStartState);
    try {
      startState = (State) UTIL.clone(x);
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).addStartState);
    }
  }
// ***** VDMTOOLS END Name=addStartState


// ***** VDMTOOLS START Name=pre_addStartState KEEP=NO
  public Boolean pre_addStartState (final State x) throws CGException {

    Boolean varRes_2 = null;
    Boolean var1_3 = null;
    var1_3 = (Boolean) stateExists(x);
    {
      if ((varRes_2 = var1_3).booleanValue()) {

        Boolean var2_8 = null;
        String par_11 = null;
        par_11 = x.getName();
        {

          String par_12 = null;
          par_12 = x.getName();
          var2_8 = (Boolean) stateExists(par_12);
        }
        varRes_2 = var2_8;
      }
    }
    return varRes_2;
  }
// ***** VDMTOOLS END Name=pre_addStartState


// ***** VDMTOOLS START Name=searchStart KEEP=NO
  public HashSet searchStart (final Integer n) throws CGException {

    if (!this.pre_searchStart(n).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in searchStart");
    sentinel.entering(((UMLSentinel) sentinel).searchStart);
    try {

      HashSet rexpr_2 = new HashSet();
      Object tmpGen_3 = null;
      Vector par_6 = null;
      par_6 = new Vector();
      par_6.add(startState);
      {

        Vector par_8 = null;
        par_8 = new Vector();
        par_8.add(startState);
        rexpr_2 = (HashSet) startState.search(par_8, new HashSet(), n);
      }
      return rexpr_2;
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).searchStart);
    }
  }
// ***** VDMTOOLS END Name=searchStart


// ***** VDMTOOLS START Name=pre_searchStart KEEP=NO
  public Boolean pre_searchStart (final Integer n) throws CGException {

    Boolean varRes_2 = null;
    {
      if ((varRes_2 = new Boolean((n.intValue()) > (new Integer(0).intValue()))).booleanValue()) 
        varRes_2 = new Boolean(!UTIL.equals(allStates, new HashMap()));
    }
    return varRes_2;
  }
// ***** VDMTOOLS END Name=pre_searchStart


// ***** VDMTOOLS START Name=stateExists KEEP=NO
  public Boolean stateExists (final String stateName) throws CGException {

    sentinel.entering(((UMLSentinel) sentinel).stateExists_u_u1_un_uString);
    try {

      Boolean cond_2 = null;
      cond_2 = new Boolean(allStates.containsKey(stateName));
      if (cond_2.booleanValue()) 
        return new Boolean(true);
      else 
        return new Boolean(false);
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).stateExists_u_u1_un_uString);
    }
  }
// ***** VDMTOOLS END Name=stateExists


// ***** VDMTOOLS START Name=stateExists KEEP=NO
  public Boolean stateExists (final State state) throws CGException {

    sentinel.entering(((UMLSentinel) sentinel).stateExists_u_u1_un_uState);
    try {

      Boolean cond_2 = null;
      cond_2 = new Boolean(allStates.containsValue(state));
      if (cond_2.booleanValue()) 
        return new Boolean(true);
      else 
        return new Boolean(false);
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).stateExists_u_u1_un_uState);
    }
  }
// ***** VDMTOOLS END Name=stateExists


// ***** VDMTOOLS START Name=getStartState KEEP=NO
  public State getStartState () throws CGException {

    sentinel.entering(((UMLSentinel) sentinel).getStartState);
    try {
      return (State) startState;
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).getStartState);
    }
  }
// ***** VDMTOOLS END Name=getStartState


// ***** VDMTOOLS START Name=isEmpty KEEP=NO
  public Boolean isEmpty () throws CGException {

    sentinel.entering(((UMLSentinel) sentinel).isEmpty);
    try {

      Boolean rexpr_1 = null;
      Boolean unArg_2 = null;
      HashSet var1_3 = new HashSet();
      var1_3.clear();
      var1_3.addAll(allStates.values());
      unArg_2 = new Boolean(!UTIL.equals(var1_3, new HashSet()));
      rexpr_1 = new Boolean(!unArg_2.booleanValue());
      return rexpr_1;
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).isEmpty);
    }
  }
// ***** VDMTOOLS END Name=isEmpty


// ***** VDMTOOLS START Name=verifyPath KEEP=NO
  public Boolean verifyPath (final Vector trace) throws CGException {

    if (!this.pre_verifyPath(trace).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in verifyPath");
    sentinel.entering(((UMLSentinel) sentinel).verifyPath);
    try {

      HashSet allSeqs = searchStart(new Integer(trace.size()));
      Boolean cond_4 = null;
      cond_4 = new Boolean(allSeqs.contains(trace));
      if (cond_4.booleanValue()) 
        return new Boolean(true);
      else 
        return new Boolean(false);
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).verifyPath);
    }
  }
// ***** VDMTOOLS END Name=verifyPath


// ***** VDMTOOLS START Name=pre_verifyPath KEEP=NO
  public Boolean pre_verifyPath (final Vector trace) throws CGException {

    Boolean varRes_2 = null;
    Boolean var1_3 = null;
    {
      if ((var1_3 = new Boolean((new Integer(trace.size()).intValue()) > (new Integer(0).intValue()))).booleanValue()) 
        var1_3 = new Boolean(UTIL.equals((State) trace.get(0), startState));
    }
    {
      if ((varRes_2 = var1_3).booleanValue()) 
        varRes_2 = new Boolean(!UTIL.equals(trace, new Vector()));
    }
    return varRes_2;
  }
// ***** VDMTOOLS END Name=pre_verifyPath


// ***** VDMTOOLS START Name=getState KEEP=NO
  public State getState (final String stateName) throws CGException {

    if (!this.pre_getState(stateName).booleanValue()) 
      UTIL.RunTime("Run-Time Error:Precondition failure in getState");
    sentinel.entering(((UMLSentinel) sentinel).getState);
    try {
      return (State) (State) allStates.get(stateName);
    }
    finally {
      sentinel.leaving(((UMLSentinel) sentinel).getState);
    }
  }
// ***** VDMTOOLS END Name=getState


// ***** VDMTOOLS START Name=pre_getState KEEP=NO
  public Boolean pre_getState (final String stateName) throws CGException {

    Boolean varRes_2 = null;
    varRes_2 = (Boolean) stateExists(stateName);
    return varRes_2;
  }
// ***** VDMTOOLS END Name=pre_getState

}
;
